Inductive BoolEval (s: State) : BoolExp -> Bool -> Prop :=
  | bool_eval_lit : forall (b:ITs.Bool),
      BoolEval s (bool_exp_lit b) b

  | bool_eval_id  : forall (i:Id)(b:Bool),
       s i = Some (bool_val b) ->  BoolEval s (bool_exp_id i) b

  | bool_eval_eq  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> BoolEval s (bool_exp_eq e1 e2) (int_eq n1 n2)

  | bool_eval_lt  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> BoolEval s (bool_exp_lt e1 e2) (int_lt n1 n2)

  | bool_eval_le  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> BoolEval s (bool_exp_le e1 e2) (int_le n1 n2)

  | bool_eval_gt  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> BoolEval s (bool_exp_gt e1 e2) (int_gt n1 n2)

 | bool_eval_gtb  : forall (e1 e2: ByteExp)(n1 n2: Byte),
      ByteEval s e1 (Some n1) -> ByteEval s e2 (Some n2) -> BoolEval s (bool_exp_gtb e1 e2) (byte_gt n1 n2)
 
 | bool_eval_eqb  : forall (e1 e2: ByteExp)(n1 n2: Byte),
      ByteEval s e1 (Some n1) -> ByteEval s e2 (Some n2) -> BoolEval s (bool_exp_eqb e1 e2) (byte_eq n1 n2)

  | bool_eval_ge  : forall (e1 e2: ArithExp)(n1 n2: Integer),
      ArithEval s e1 n1 -> ArithEval s e2 n2 -> BoolEval s (bool_exp_ge e1 e2) (int_ge n1 n2)

  | bool_eval_not : forall (e1: BoolExp)(b1: Bool),
      BoolEval s e1 b1 -> BoolEval s (bool_exp_not e1) (bool_not b1)

  | bool_eval_and : forall (e1 e2: BoolExp)(b1 b2: Bool),
      BoolEval s e1 b1 -> BoolEval s e2 b2 -> BoolEval s (bool_exp_and e1 e2) (bool_and b1 b2)

  | bool_eval_or  : forall (e1 e2: BoolExp)(b1 b2: Bool),
      BoolEval s e1 b1 -> BoolEval s e2 b2 -> BoolEval s (bool_exp_or e1 e2) (bool_or b1 b2)
.